package gov.nasa.jpf.symbc.modelcounter.sampler;

import java.util.HashSet;
import java.util.Set;

import org.apfloat.Apfloat;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.symbc.modelcounter.sampler.EvaluationVisitor.Result;
import gov.nasa.jpf.symbc.numeric.Constraint;
import gov.nasa.jpf.symbc.numeric.PathCondition;

/**
 * A sampling model counter that is equivalent to a random tester.
 * 
 * @author Jaco Geldenhuys
 */
public class RandomTester extends Sampler {

	/**
	 * The collection of test inputs.
	 */
	private Set<Assignment> samples = null;

	/**
	 * A visitor for constraints/expressions used to determine whether samples
	 * are true or false.
	 */
	protected EvaluationVisitor evaluator;

	/**
	 * Construct a new random tester.
	 * 
	 * @param config
	 *            a JPF configuration
	 */
	public RandomTester(Config config) {
		super(config);
		long y = config.getLong("symbolic.prob_test_sample_size",
				Long.MAX_VALUE);
		if (y != Long.MAX_VALUE) {
			sampleCount = y;
		}
		System.out.println("symbolic.prob_test_sample_size=" + sampleCount);
		samples = new HashSet<Assignment>();
		for (int i = 0; i < sampleCount; i++) {
			samples.add(new MapAssignment(this));
		}
		evaluator = new EvaluationVisitor(null);
	}

	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * gov.nasa.jpf.symbc.modelcounter.ModelCounter#getConditionalProbability
	 * (gov.nasa.jpf.symbc.numeric.PathCondition, double)
	 */
	@Override
	public Apfloat getConditionalProbability(PathCondition pathCondition,
			Apfloat parentProb) {
		long t = sampleCount; // number of samples that evaluate as true
		for (Assignment a : samples) {
			for (Constraint c = pathCondition.header; c != null; c = c
					.getTail()) {
				evaluator.reset(a);
				c.accept(evaluator);
				if (evaluator.getResult() != Result.TRUE) {
					t--;
					break;
				}
			}
		}
		Apfloat pr = new Apfloat(t).divide(new Apfloat(sampleCount).multiply(parentProb));
		System.out.println("## " + t + " / " + sampleCount + " / " + parentProb + " == " + pr);
		return pr;
	}

	@Override
	public Apfloat getProbability(Set<PathCondition> pathConditions) {
		// TODO Auto-generated method stub
		return null;
	}

}
